$\forall$${\it es}$:ES. es{-}T(${\it es}$) $\in$ Id$\rightarrow$Id$\rightarrow$Type